open SWIMv2_Model as _
open util/ordering[State] as timeState


/**------------**/
/** System **/
/**------------**/

sig State
{
	today: one Date,
	users: set User,
	objects: set Object
}

/**------------------**/
/** Operations **/
/**------------------**/

pred sendMessages[s,s': State,  senderUser: User, recipientUsers: set RegisteredUser ]
{
	one m: Message
	{ 
		m not in s.objects &&
		m in s'.objects &&
		m.sender = senderUser &&
		m.recipient = recipientUsers &&
		m.creationDate = s'.today		
	}
}

pred banUsers[s,s': State, a: Admin, ru: RegisteredUser, bu: BannedUser]
{	
	a in s.users &&
	ru not in Admin &&
	ru not in s'.users &&
	bu in s'.users	
}

pred leaveFeedback[s,s': State, ru, ru': RegisteredUser]
{
	ru  in s.users &&
	ru' in s.users &&
	ru' in s'.users &&
	one f: Feedback
	{
		f not in s.objects &&
		f in s'.objects &&
		f.leftBy = ru &&
		f in ru'.feedback &&
		f.creationDate = s'.today	
	}
}

pred addAbilities[s,s' : State, a: Admin]
{
	a in s.users &&
	one ab: Ability
	{	
		ab not in s.objects &&
		ab in s'.objects &&
		ab.creationDate = s'.today
	}
}

pred addHelpRequest[s,s' : State,  ru, ru': RegisteredUser]
{
	ru in s.users &&
	ru in s'.users &&
	ru' in s.users &&
	ru' in s'.users &&
	one h: HelpRequest
	{	
		h not in s.objects &&
		h in s'.objects &&
		h.creationDate = s'.today
	}
}

/**---------**/
/** Facts **/
/**---------**/

//status are oredered by day
fact RightOrder
{
	all s: State | let s' = s.next
	{
		gt[s'.today, s.today]
	}
}

//every user is in at least one status
fact AllUsersInState
{
	all u:User
	{
		some s:State | u in s.users
	} 
}

/** Founder **/

//founder is always present
fact AlwaysOnefounder
{
	all s: State | Founder in s.users
}

/** Banned Users **/

//User can't be banned in a satus with a date which is later than his end ban date
fact NoExpiredbanned
{
	all s: State | no bu : BannedUser
	{
		bu in s.users  && gte[s.today,bu.endBan]
	}
}

//Exists a RegisteredUser befor that the banned user and he's the same at the end of his ban
//Double ban of a user is not considered
fact WasRegisteredUser
{
	all bu: BannedUser | one u: RegisteredUser
	{
		u not in Admin &&
		all s: State
		{
			(
				bu in s.users implies 
				(
					((bu in s.prev.users && u not in s.prev.users)  || u in s.prev.users) && u not in s.users
				)
			)
			&&  
			(
				gte[s.today, bu.endBan] implies u in s.users
			)
		}
	}
}

/** Objects **/

//No objects are found before that date
fact NoFutureComunication
{
	all s: State | no o : Object
	{
		o in s.objects  && lt[s.today,o.creationDate]
	}
}

//Object exists in the satus with the same date of its creation
fact ExistNow
{
	all s:State, o: Object
	{		
		o.creationDate = s.today implies o in s.objects 
	}
}

//No state where an object doesn't exist between two status where it exists
fact noPopUpExistence
{
	all o: Object | no s: State
	{
		some is,fs: State
		{
			o in is.objects && 
			o in fs.objects && 	
			o not in s.objects &&
			gt[s,is] && lt[s,fs]
		}
	}
}

//The abilities remain
fact abilitiesForever
{
	all s: State - timeState/last
	{
		all a: Ability 
		{
			(a in s.objects) implies a in s.next.objects
		}
	}	
}

//Messages exist only when recipient and sender exist
fact SendToExistingPeople
{
	all m: Message | some s: State
	{
		m.creationDate = s.today &&
		m.sender in s.users &&
		m.recipient in s.users
	}
}

//HelpRequests exist only in status where exist who recieved them
fact HelpedBySomeone
{
	all s: State | all hr: HelpRequest
	{
		hr in s.objects implies hr.involves in s.users
	}
}

//When a request of help is sent, we are in the system
fact AskHelpWhileAlive
{
	all s: State | all hr: HelpRequest
	{
		hr.creationDate= s.today implies hr.generatedBy in s.users
	}
}

/** --------------- **/
/** Predicates **/
/** --------------- **/

//I show message creation
pred creationMessage[m1_appear:Message]
{
	m1_appear in univ
}

//I show firends existance
pred friends [f1: User, f2:User, f3:User, f4:User]
{
	f1 in f2.friends
	f3 in f2.friends
	f4 in f3.friends
}


/**-----------------------------**/
/** Execution Comands **/
/**-----------------------------**/

run {}

run friends for 6

run sendMessages for 10

run banUsers for 10

run leaveFeedback for 10

run addAbilities for 10

run addHelpRequest for 10
